//胡玉来，4.3
//耿浩诚，4.8
//林峰玉，4.9

//4.3
//基本进程的逻辑已经实现
//跑了只存在一个组件进程的情况，能够跑通
//互斥属性的验证也能够通过

//下一步：
//验证多个组件进程同时运行的情况
//1.验证pdf中的正确性属性6，7
//2.验证pdf中的断言

//4.8
//性质6,7可以验证成功；
//组件访问模式为“函数调用”这个断言不成功；
//不知怎么添加：应为抢占请求，主进程退出时的结束请求只能由用户服务线程响应这个断言。

//4.9
//加入了对于性质1，断言的验证
//基本逻辑无误，可以通过初步的检测
//
//


//控制队列和数据队列的容量
#define MAX_CONTROL_QUEUE_SIZE 10
#define MAX_DATA_QUEUE_SIZE 10
#define MAX_COMP_QUEUE_SIZE 10

//定义常数类型:抢占请求，数据请求，结束请求，响应抢占请求，响应数据请求，响应结束请求，函数调用模式，请求服务模式
mtype={ preempt,end,data_req,response_preempt,response_end,response_data,func_call,service_req}


//控制队列 
chan Control_queue=[MAX_CONTROL_QUEUE_SIZE] of {mtype,int};
//数据队列 
chan Data_queue=[MAX_CONTROL_QUEUE_SIZE] of {mtype,int};
//组件模式队列
chan Comp_queue=[MAX_COMP_QUEUE_SIZE] of {mtype, int};


//定义的互斥锁
byte Control_mutex=0;//控制队列
byte Data_mutex=0;//数据队列
byte Clean_Mutex=0;//清理组件
byte Create_Mutex=0;//创建服务进程
byte Fun_Call_Mutex=0;//函数调用模型执行代码

byte Comp_Lock=0;//设置调用模式锁

bit cleaned=1;//已清理
bit service_end=1;//服务已退出
bit service_create=0;//服务未创建

//LTL
ltl mutex_1 {[](Control_mutex<2)}
ltl mutex_2 {[](Data_mutex<2)}
ltl mutex_3 {[](Clean_Mutex<2)}
ltl mutex_4 {[](Create_Mutex<2)}
ltl mutex_5 {[](Fun_Call_Mutex<2)}

ltl prop_6 {[](service_end -> cleaned)} //服务退出前，应有清理操作
ltl prop_7 {[](!(service_create) -> cleaned)} //服务创建前，现有服务已清理

//root进程
//proctype root()


//内核服务进程
proctype kernel_serve_proc()
{
	service_create=1;
	//设置内核访问模式为函数调用
	atomic{Comp_Lock==0->Comp_Lock++;}
	mtype access_mode=func_call;
	Comp_queue!access_mode,_pid;
	Comp_Lock--;

	int receive_pid;//存储进程号

	do
	::Control_queue??preempt,receive_pid->
		
		{
		assert(access_mode==preempt);
		//assert(1>2);

		atomic{Clean_Mutex==0->Clean_Mutex++;cleaned=1;}
		printf("内核服务线程清理组件\n");
		Clean_Mutex--;
		
		//响应请求
		atomic{Control_mutex==0->Control_mutex++;}
		Control_queue!response_preempt,receive_pid; //
		Control_mutex--;
		
		//内核服务线程结束；
		service_end=1;
		service_create=0;
		break;
		}
		
	::Data_queue??data_req,receive_pid->	
		{
		atomic{Fun_Call_Mutex==0->Fun_Call_Mutex++;};//使用函数调用模式处理请求
		//调用处理请求函数
		Fun_Call_Mutex--;
		
		//响应数据请求
		atomic{Data_mutex==0->Data_mutex++;};
		Data_queue!response_data,receive_pid;
		Data_mutex--;
		}
	::timeout->printf("end!!\n")->break;
	od
	
	//设置访问模式为函数调用
	atomic{Comp_Lock==0->Comp_Lock++;}
	Comp_queue??access_mode,_pid;
	Comp_Lock--;
}

//普通进程
proctype general_proc()
{
	int receive_pid;

	atomic{Comp_Lock==0->Comp_Lock++;}
	mtype access_mode=service_req;
	Comp_queue!access_mode,_pid;
	Comp_Lock--;

	//执行应用代码
	printf("普通进程执行应用代码\n");
	
	
	//发送数据请求
	atomic{Data_mutex==0->Data_mutex++;}
	Data_queue!data_req,_pid;	
	Data_mutex--;
	
	//等待响应
	do
	::Data_queue??response_data,receive_pid->
		if
		::(receive_pid==_pid)->break;
		::else->
		{
			atomic{Data_mutex==0->Data_mutex++;};
			Data_queue!response_data,receive_pid;
			Data_mutex--;
		}
		fi
	od

	//删除当前进程的访问模式
	atomic{Comp_Lock==0->Comp_Lock++;}
	Comp_queue??access_mode,_pid;
	Comp_Lock--;
}

//组件主进程
proctype comp_main_proc()
{
	int receive_pid;

	//发出抢占请求
	atomic{Control_mutex==0->Control_mutex++;};
	Control_queue!preempt,_pid;
	Control_mutex--;
	
	//等待响应
	do
	::Control_queue??response_preempt,receive_pid->
		if
		::(receive_pid==_pid)->break;
		::else->
		{
			atomic{Control_mutex==0->Control_mutex++;};
			Control_queue!response_preempt,receive_pid;
			Control_mutex--;
		}
		fi
	od

	
	
	//设置访问模式为函数调用
	atomic{Comp_Lock==0->Comp_Lock++;}
	mtype access_mode=func_call;
	Comp_queue!access_mode,_pid;
	Comp_Lock--;
	
	
	//创建用户服务线程（互斥）
	atomic{Create_Mutex==0->Create_Mutex++;service_end=0;};
	run usr_serve_proc(_pid);//创建服务进程并启动
	Create_Mutex--;
	
	
	
	atomic{Fun_Call_Mutex==0->Fun_Call_Mutex++;}
	//函数调用方式执行应用代码
	Fun_Call_Mutex--;
			
	
	//发出结束请求
	atomic{Control_mutex==0->Control_mutex++;}
	Control_queue!end,_pid;
	Control_mutex--;
	
	//等待请求处理完成
	do
	::Control_queue??response_end,receive_pid->
		if
		::(receive_pid==_pid)->break;
		::else->
		{
			atomic{Control_mutex==0->Control_mutex++;};
			Control_queue!response_end,receive_pid;
			Control_mutex--;
		}
		fi
	od
	
	//等待用户服务进程结束
	//应该需要写一个进程服务结束？

	atomic{Comp_Lock==0->Comp_Lock++;}
	Comp_queue??access_mode,_pid;
	Comp_Lock--;
}

//用户服务进程
proctype usr_serve_proc(int main_pid) //按顺序取值
{
	
	mtype access_mode;
	service_create=1;
	int receive_pid;//存储进程号

	do
	::Control_queue??preempt,receive_pid ->//读取抢占类型
		
		atomic{Clean_Mutex==0->Clean_Mutex++;cleaned=1;}
		//清理组件
		Clean_Mutex--;
		
		//设置组件模式为请求服务
		atomic{Comp_Lock==0->Comp_Lock++;}
		access_mode=service_req;
		Comp_queue!access_mode,_pid;
		Comp_Lock--;
		
		//响应请求
		atomic{Control_mutex==0->Control_mutex++;}
		Control_queue!response_preempt,receive_pid;
		Control_mutex--;
		
		//内核服务线程结束；
		service_end=1;
		service_create=0;
		break;
		
		
	::Control_queue??end,receive_pid-> //end
		if
		:: (receive_pid == main_pid)->//进程号和主进程相同
		{
		atomic{Clean_Mutex==0->Clean_Mutex++;cleaned=1;}
		//清理组件
		printf("清理组件");
		Clean_Mutex--;
		
		//创建内核服务线程并启动
		atomic{Create_Mutex==0->Create_Mutex++;service_end=0;};
		run kernel_serve_proc(); // run kernel 
		Create_Mutex--;
			
		//响应结束请求
		atomic{	Control_mutex==0->Control_mutex++;}
		Control_queue!response_end,receive_pid;
		Control_mutex--;
		service_end=1;
		break;
		}
		::else->
		{
			atomic{Control_mutex==0->Control_mutex++;};
			Control_queue!end,receive_pid;
			Control_mutex--;
		}
		fi
		
	::Data_queue??data_req,receive_pid->	
		{
		int tmp_pid;
		mtype tmp_access_mode;
		int first_pid;
		atomic{Comp_Lock==0->Comp_Lock++;}
		Comp_queue?tmp_access_mode,first_pid;
		Comp_Lock--;
		atomic{Comp_Lock==0->Comp_Lock++;}
		Comp_queue!tmp_access_mode,first_pid;
		Comp_Lock--;
		
		do
		::Comp_queue?tmp_access_mode,tmp_pid->
		{
			if 
			::(tmp_pid == receive_pid)->
			{
				atomic{Comp_Lock==0->Comp_Lock++;}
				Comp_queue!tmp_access_mode,tmp_pid;
				Comp_Lock--;
				break;
			}
			::(tmp_pid == first_pid)->
			{
				atomic{Comp_Lock==0->Comp_Lock++;}
				Comp_queue!tmp_access_mode,tmp_pid;
				Comp_Lock--;
				break;
			}
			::else->
			{
				atomic{Comp_Lock==0->Comp_Lock++;}
				Comp_queue!tmp_access_mode,tmp_pid;
				Comp_Lock--;
			}
			fi
		}
		od
		
		assert(tmp_access_mode==func_call); //函数调用断言
		atomic{Fun_Call_Mutex==0->Fun_Call_Mutex++;};//使用函数调用模式处理请求
		//调用处理请求函数
		Fun_Call_Mutex--;
		
		//响应数据请求
		atomic{Data_mutex==0->Data_mutex++;}
		Data_queue!response_data,receive_pid;
		Data_mutex--;
		}

	od

	atomic{Comp_Lock==0->Comp_Lock++;}
	Comp_queue??access_mode,_pid;
	Comp_Lock--;
}



init 
{
  run general_proc()
  run comp_main_proc()
  run kernel_serve_proc();
}